Explicitly make the current commit be the one against which the git tag is made#37
Explicitly make the current commit be the one against which the git tag is made#37wilfwilson merged 1 commit intomainfrom
Conversation
…ag and release should be made Resolves #36.
|
I just another test release of the Semigroups package on my fork, v7.8.11 from the I can confirm that the tag was made against the correct commit, so I believe that this PR is correct and ready to be merged. |
stertooy
left a comment
There was a problem hiding this comment.
LGTM.
Out of curiosity: is there any difference between using github.sha versus github.ref_name ?
|
From the documentation:
So for some workflow runs, such as for a job triggered by On the other hand, I think |
Resolves #36.